a:, b:. a | b & b | a  a<b & a | b 

latex

Definitions	P  Q, P  Q, x:A. B(x), AB, A, False, P  Q, P & Q, b | a, Prop, , t  T, , Dec(P), P  Q, a ~ b
Lemmas	nat plus inc, assoced nelim, assoced weakening, divides weakening, decidable int equal, divisor bound, nat wf, nat plus wf, divides wf, not wf